We now introduce the syntax and semantics of \hof. 
We use $a,b,c$ to range over names, and $x,y,z$ to
range over variables; the sets of names and variables are  disjoint.
%The continuation of an input is a \emph{thread}: 
%threads depend on the input argument $x$.
%Here is where the limitation to the capabilities of higher-order processes takes place: 
%threads represent the limited uses when forwarding a message. 
%{\small
\[
\begin{array}{rcll}
P,\,Q & :: = &  \Ho{a}{x_1 \parallel \dots \parallel x_k \parallel P} \  \quad (\mbox{with}~k \geq 0, ~\fv{P} = \emptyset) ~~ & \mbox{output}\\[\mypt]
 & \mid &  \inp a x . P & \mbox{input prefix} \\[\mypt]
 & \mid &  P \parallel Q & \mbox{parallel composition} \\[\mypt]
 & \mid &  x  & \mbox{process variable} \\[\mypt]
 & \mid & \nil & \mbox{nil}\\[\mypt]
\end{array} 
 \]
%}
An input $\inp a x.P$ binds the free occurrences of $x$ in $P$.
This is the only binder in the language.
We write $\fv P$ and $\bv P$ for the set of free and bound variables in $P$, respectively.
%and  $\bv P$ for the %set of its bound variables.  
%We identify processes up to a renaming of bound  variables.
A process is \emph{closed} if it does not have free variables. 
%In a statement, a name is \emph{fresh} if it is not among the names of the objects (processes, actions, etc.) of the statement. 
% We write $\PrOp$ for the set of all processes, and $\PrClo$ for the subset
% of {closed} processes.
When $x \not \in \fv P$,
we abbreviate $\inp a x . P$ as $a . P$.
We also abbreviate $\Ho{a}{\nil}$ as $\overline{a}$,
$P_1\! \parallel\! \ldots\! \parallel\! P_k$ as $\prod_{i=1}^k \!P_i$,
and omit trailing occurrences of $\nil$. Hence, an output action 
can be written as $\Ho{a}{\prod_{k \in K} x_k	\! \parallel\! P}$.
%Simi\-larly, w
We write $\prod^n_1 \!P$ 
as an abbreviation 
for the parallel composition of $n$ copies of $P$. 
Further, $P{\sub Q x}$ denotes the substitution of the free occurrences of 
$x$ with process ${Q}$ in $P$. 


%Now we describe the 
%The Labeled Transition System (LTS) of \hof is defined on closed processes.
The %Labeled Transition System (LTS) 
LTS
of \hof is defined 
in Figure \ref{fig:ltswithalpha}.
%as follows:
It decrees there are three forms of transitions: $\tau$ transitions $P  \arr\tau P'$;
input transitions $P \arr{\ia a x} P'$, meaning that  $P$
can receive   at  $a$ a process that
will replace $x$ in the continuation $P'$; and
output transitions $P \arr{\Ho{a}{P'}}P''$ meaning that $P$ emits
$P'$ at $a$, and in doing so it
evolves to $P''$.
We use $\alpha $ to indicate a generic label of a transition. 
The notions of free and bound variables extend to labels as expected.

%\begin{figure}[h]
\begin{figure}[t]
$$\mathrm{\textsc{Inp}}~~~{\inp a x. P} \arr{\ia a x  }  {P } \qquad \qquad \mathrm{\textsc{Out}}~~~{\Ho{a}{P}} \arr{\Ho a P  }  {\nil}$$
$$
\rightinfer	[\textsc{Act1}]
			{P_1 \parallel P_2 \arr\alpha P'_1 \parallel P_2}
			{P_1 \arr\alpha P_1'  \andalso \bv \alpha \cap \fv{ P_2} = \emptyset}
\qquad
\rightinfer	[\textsc{Tau1}]
			{P_1 \parallel P_2 \arr\tau  P'_1 \parallel P'_2 \sub{P}{x}}
			{P_1 \arr{\Ho{a}{P}} P_1' \andalso P_2 \arr{\iae a (x)} P'_2}
$$
\caption[An LTS for \hof]{An LTS for \hof.
Rules \textsc{Act2} and \textsc{Tau2}, the symmetric counterparts of 
\textsc{Act1} and \textsc{Tau1}, have been omitted.} \label{fig:ltswithalpha}
%\end{table}
\end{figure}

% We write  $P \arr{\iae a M}Q $ if 
% $P \arr{\ia a x}Q' $ and $Q' \sub Mx = Q$ (this form of action is
% called  \emph{early input} in the literature).  
% In the remainder, $\alpha $ may also be an early input. 
% Further, with some abuse of notation, if $\alpha  = {\ia a x}$ then
% $\alpha \sub Qx = aQ$.

 
% Finally we define  the \emph{barbs}, and write $P \dwa_a$ if there is
% $\alpha $ and $P'$ s.t.\
% $P \arr\alpha P'$ where $\alpha $ is an input or output action at $a$.

%\begin{remark}\label{r:alpha}
%Since we consider closed processes,  in rule \textsc{Act1}, $P_2$ has no free variables and
%no side conditions are necessary. 
%As a consequence, 
%This is important because it entails the fact that 
%alpha-conversion is not needed.
%\end{remark}






%TERMINATION VS CONVERGENCE

%Given a process $P$, its inter1nal runs $P \pired P_1 \pired P_2 \pired \ldots$ are given by 
%sequences of reductions.
%\emph{Reductions} $P \pired P'$ are defined as $P \arr{\tau} P'$.
The internal runs of a process are given by sequences of \emph{reductions}.
Given a process $P$, its reductions $P \pired P'$ are defined as $P \arr{\tau} P'$.
%the sequences of $\tau$ label transitions. 
We denote with $\pired^*$ the reflexive and transitive closure of $\pired$; notation 
 $\pired^j$ is to stand for a sequence of $j$ reductions.
We use $P \nrightarrow$ to denote that there is no $P'$ such  that $P \pired P'$. %,  $P$ is said to be \emph{dead}. 
Following \cite{Busi09} we now define process convergence and process termination. 
%Intuitively a process $P$ converges if there exists an internal run with a dead process. $P$ \emph{terminates} if all its internal runs converge.
Observe that termination implies convergence while the opposite does not hold.

\begin{mydefi}\label{d:term-conv}
Let $P$ be a \hof process. 
\begin{enumerate}
 \item 
We say that $P$ \emph{converges}  iff there exists $P'$ such that $P \pired^* P'$ and $P' \nrightarrow$.
\item 
We say that $P$ \emph{terminates} iff there exist no $\{P_i\}_{i \in \mathbb{N}}$ such that $P_0\! =\! P$ and $P_j\! \pired \! P_{j+1}$ for any $j$.
\end{enumerate}
\end{mydefi}
%Termination and convergence are sometimes also referred to as \emph{universal} and \emph{existential} termination, respectively.
